es:ES, ff:FIFO, p:(E), i, j:ff.C, e:E. [e: i p j]  [ff.Sender(i,e): j p i] 

latex

Definitions	x:A. B(x), FIFO, , P  Q, [e: i p j], [e: i p j], P & Q, A c B, t  T
Lemmas	es-E wf, fifoC wf, es-state wf, es-loc wf, fifo wf, event system wf